Nuprl Lemma : select_cons_tl_sq
11,40
postcript
pdf
T
:Type,
x
:
T
,
l
:(
T
List),
i
:int_seg(0; ||
l
||). sqequal(cons(
x
;
l
)[(
i
+ 1)];
l
[
i
])
latex
Definitions
True
,
P
Q
,
sq_type(
T
)
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
t
T
,
guard(
T
)
,
int_seg(
i
;
j
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
T:Type, x:T, l:(T List), i:int_seg(0; ||l||). sqequal(cons(x; l)[(i + 1)]; l[i]) T:Type, x:T, l:(T List), i:int_seg(0; ||l||). sqequal(cons(x; l)[(i + 1)]; l[i]) 
Qx:A. B(x)
T